1. $A$ : Type
\\[0ex]2. $e$ : $A$
\\[0ex]3. $H$ : $A$$\rightarrow$Type
\\[0ex]4. $H$($e$)
\\[0ex]5. $A$ $\in$ Type
\\[0ex]$\vdash$  $e$ $\in$ $A$